Integrated circuits have grown in complexity and number of components such that the typical design methodology requires a series of design levels between a general logic circuit description and the manufacturing level description. Examples of the design levels are the high level register-transfer-level (RTL) description and the low level netlist description. The RTL description is synthesized into a netlist description, which is then converted into a physical semiconductor circuit layout. The RTL description describes the operation of the integrated circuit under design independent of any particular technology. The netlist is a data structure representation of the electronic logic system, which describes how standard cells and blocks are interconnected.
Because of the number of design levels, design verification is required to verify that the optimizations and transformations introduced during the design process do not alter the intended design logic. One common type of design verification is combinational Boolean equivalence checking. Two design levels, known as the reference and the implementation, such as the RTL description and the netlist description, are broken up into combinatorial, cycle-free blocks, often termed “logic cones.” Formal techniques are used to compare and verify the logic cones from the reference and the implementation. The comparison of all corresponding logic cones demonstrates the equivalence of the reference and the implementation, without the need to apply simulation test patterns.
An important part of combinational Boolean equivalence checking is identifying and matching compare points in the reference and the implementation. Compare points are among the combinational logic end points used in verification. Compare points include output ports, latches, and registers. Matching compare points assures that logic cones are only compared for equivalence if they are expected to be equivalent in a correct design.
Compare point matching techniques can be broadly classified as function-based and non-function-based methods. Function-based methods implicitly enumerate all compare point combinations and pair functionally equivalent compare points. A logic function is constructed for each latch and the logic function of each latch is checked against the logic functions of other latches until all the latches are paired. Non-function-based methods use heuristic methods to match the compare points. Equivalence of pairs of compare points is guessed based on evidence such as similarity of compare point names or logic topology. The guessing continues until all the compare points are paired.
Both the function-based and non-function-based methods present problems when used alone. The function-based methods are exact methods, but require expensive, non-trivial computation. The function-based methods require at least the performance of a complete equivalence check. In the worst case, the computation can time out and terminate before the matching and verification is complete, resulting in failure without any useful result. The non-function-based methods can fail on encountering particular conditions in the reference and the implementation.
It would be desirable to have a system and method of state point correspondence with constrained function determination that would overcome the above disadvantages.